| Definitions | left  right, es realizer ind Rplus compseq tag def,  , es realizer ind Rnone compseq tag def, @loc x initially v:T, es realizer ind Rinit compseq tag def, deq-member(eq;x;L), EqDecider(T), only events in L send on lnk with tag, es realizer ind Rsframe compseq tag def, @loc effect knd(v:T) x := f State(ds) v , es realizer ind Reffect compseq tag def, p   q, f(x)?z, S  T, (x  l), rec(x.A(x)), f || g, <a,b>, f(x), x dom(f), False, P Q, sends knd(v:T) on l:tagged(g,State(ds),v):dt, es realizer ind Rsends compseq tag def, f g, lnk-decl(l;dt), source(l), @loc precondition for a(v:T):P State(ds) v, es realizer ind Rpre compseq tag def, locl(a), @loc: k writes only members of L, es realizer ind Raframe compseq tag def, @loc: k sends only on links in L, es realizer ind Rbframe compseq tag def, @loc: only members of L read x, R-occurs(R;i;z), R-loc(R), Rds(R), Rda(R), R-base-domain(R), p = q, R-frame-compat(A;B), R-interface-compat(A;B), Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), Rframe?(x1), Rframe-x(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Reffect-x(x1), Raframe-L(x1), Reffect-ds(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsframe-tag(x1), Rsends-g(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rrframe?(x1), Rrframe-x(x1), Rpre-ds(x1), Rpre-a(x1), Rrframe-L(x1), Reffect?(x1), Reffect-knd(x1), Reffect-T(x1), Rsends?(x1), Rsends-knd(x1), Rsends-l(x1), Rsends-dt(x1), Rsends-T(x1), i=j, es realizer ind Rframe compseq tag def, es realizer ind Rrframe compseq tag def, left+right, Unit, P   Q, P  Q, {x:A| B(x) }, f(a), es realizer ind,  x,y,z,w. t(x;y;z;w), x,y,z,u,v,w. t(x;y;z;u;v;w), x:A B(x), DeclaredType(ds;x), x,y,z,w,v. t(x;y;z;w;v), a:A fp B(a), State(ds), IdLnk, x,y,z. t(x;y;z), p  q, A || B, Realizer, @loc only events in L change x:T, type List,  T, Atom$n, s ~ t, SQType(T), P Q, {T}, a = b, IdDeq, x : v, x:A B(x), KindDeq,  x:A. B(x), Void, , x. t(x), x.A(x), Top, Knd,  ,  b, A, Type,  b,  x:A. B(x), Prop, s = t, Id, P & Q, A & B, True, t T |